monadic second-order logic

Definition

Monadic second-order logic (MSO) is the fragment of second-order logic where second-order quantification is limited to quantification over sets (set predicates) e.g. $\forall X.\varphi(X)$

In other words, MSO confines second-order quantification to monadic predicates.

Notes

• a predicate symbol $P$ is monadic if its arity is $1$
  • e.g. $Y$ in $\forall x . \exists Y . \forall y . Y(y) \leftrightarrow x= y$
• MSO confines second-order quantification to monadic predicates

See also

• monad
• second-order logic
• existential second-order logic

References

1. https://en.wikipedia.org/wiki/Monadic_second-order_logic
2. https://plato.stanford.edu/entries/logic-higher-order/#SyntSecoOrdeLogi
3. https://www-sop.inria.fr/members/Martin.Avanzini/teaching/2021/AL/slides/w2.pdf